package cfsmon.logic.dfm;

import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.Map;
import java.util.Queue;
import java.util.Set;

import org.apache.log4j.Logger;

import cfsmon.common.Event;

public class DfmOptimizer {

	private static Logger logger = Logger.getLogger(DfmOptimizer.class);
	
	public static IDfm optimize(IDfm logicObject) {
		
		if (logicObject != null){
			logger.debug("Removing transitions from final states.");
			removeTransitionsFromFinalStates(logicObject);
			logger.debug("Reducing DFM to reachable states.");
			reduceToReachableStates(logicObject);
			
			// validity checks
			if (!hasAtLeastOneFinalState(logicObject)){
				logger.info("There is no reachable error state in the monitor. The resulting property is a tautology.");
				// nevertheless the property is valid.
			}
			
			if (!creatingEventsSatisfied(logicObject)){
				logger.error("Aborting compilation.");
				return null;
			}
			
			if (!noInitalStateIsFinal(logicObject)){
				logger.error("The initial state is also an error state in the monitor. This is not allowed in CFSMon.");
				return null;
			}
			
		}
		
		return logicObject;
	}
	
	/**
	 * If a trace induced by an input sequence contains a final state then
	 * there exists a finite prefix of that sequence that contains exactly one final state
	 * and ends with a final state.
	 * Thus for every dfm there exists an equivalent dfm with respect to final state
	 * reachability of traces that has no outgoing transitions in final states.
	 * This Method removes all outgoing transitions from final states and enables a reflexive
	 * transition for every input symbol in that states.
	 */
	private static void removeTransitionsFromFinalStates(IDfm dfm){
		for (DfmState s : dfm.getFinalStates()){
			s.setDefaultTransition(s);
			s.getTransitions().clear();
		}
	}
	
	private static void reduceToReachableStates(IDfm dfm){
		Set<DfmState> reached = new HashSet<DfmState>();
		
		Queue<DfmState> stateQueue = new LinkedList<DfmState>();
		
		// determine reachable set
		
		stateQueue.add(dfm.getInitialState());
		
		while (!stateQueue.isEmpty()){
			DfmState s = stateQueue.poll();
			reached.add(s);
			
			// default transition
			if (!s.getTransitions().keySet().containsAll(dfm.getEvents().values())){
				// default transition can be triggered
				if (!reached.contains(s.getDefaultTransition()) && !stateQueue.contains(s.getDefaultTransition())){
					stateQueue.add(s.getDefaultTransition());
				}
			}
			// event transitions
			for (DfmState to : s.getTransitions().values()){
				if (!reached.contains(to) && !stateQueue.contains(to)){
					stateQueue.add(to);
				}
			}			
		}
		
		// drop unreachable states
		Iterator<Map.Entry<String, DfmState>> it = dfm.getStates().entrySet().iterator();
		while (it.hasNext()){
			Map.Entry<String, DfmState> entry = it.next();
			if (!reached.contains(entry.getValue())){
				logger.debug("Removed unreachable state " + entry.getKey() + ".");
				it.remove();
			}
		}
		
		// drop unreachable final states
		Iterator<DfmState> finalIt = dfm.getFinalStates().iterator();
		while (finalIt.hasNext()){
			DfmState s = finalIt.next();
			if (!reached.contains(s)){
				finalIt.remove();
			}
		}
	}
	
	private static boolean hasAtLeastOneFinalState(IDfm dfm){
		return !dfm.getFinalStates().isEmpty();
	}
	
	private static boolean noInitalStateIsFinal(IDfm dfm){
		return !dfm.getFinalStates().contains(dfm.getInitialState());
	}
	
	/**
	 * Checks if every event triggering a transition from the initial state
	 * into a non-initial and non-final state has all parameters known to the DFM.
	 * This is necessary for a simple approach to managing monitor instances.
	 * @return True if and only if the predicate is satisfied
	 */
	private static boolean creatingEventsSatisfied(IDfm dfm){
		if (!dfm.getEvents().isEmpty()){
			DfmState init = dfm.getInitialState();
			// default transition
			if (!init.getTransitions().keySet().containsAll(dfm.getEvents().values())){
				// default transition can be triggered
				if (init.getDefaultTransition() != init
						&& !dfm.getFinalStates().contains(init.getDefaultTransition())){
					logger.error("Constructing default transition detected. Please remove constructing default transitions from the initial state.");
					return false;
				}
			}
			// event transitions
			for (Event e : init.getTransitions().keySet()){
				if (init.getTransitions().get(e) != init
						&& !dfm.getFinalStates().contains(init.getTransitions().get(e))){
					// e is constructing
					if (!e.parameters.containsAll(dfm.getParameters().values())){
						// e lacks required parameters
						logger.error("Non-constructing transition with event <" + e + "> for the initial state detected.");
						return false;
					}
				}
			}
		}
		return true;
	}

}
